1. Technical Field
The present invention relates generally to a method, system, and computer program product for creating electronic circuits. More particularly, the present invention relates to a method, system, and computer program product for verifying the operations of a circuit by verifying a state transition machine representation of the circuit.
2. Description of the Related Art
Electronic circuits can be configured to perform mathematical computations. For example, a logic circuit in a microprocessor's integrated circuit may be configured to multiply two integers by manipulating their binary representation in a series of steps according to an algorithm.
Before the circuit can be designed for performing a computation, the series of steps according to a corresponding algorithm are represented in the form of a state transition machine (STM). A state transition machine is also known as a finite state machine, a finite state automaton, or simply a state machine.
An STM includes a set of states. A transition from one state to another state is called a state transition, and occurs in the STM when certain conditions are met. A state can receive an input, and produce an output. The output of one state may be an input for another state. Conditions that exist before a state transition are called pre-conditions. Conditions that exist after a state transition occurs are called post-conditions. For example, an input and pre-conditions trigger the operation of an STM, which performs state transitions according to the conditions configured in the STM, and produces an output and post-conditions.
Operating an STM is the process of supplying the STM an input and a set of pre-conditions, performing state transitions of the STM, and generating an output and post-conditions. Depending on the conditions programmed for the various state transitions, operating an STM can take a significant amount of time. An STM taking several seconds, that is a billion machine cycles or more, to generate an output is not uncommon.
The operation of an STM can be further affected by the size of data used in the operation. For example, where an STM may perform a computation using sixty four bit inputs in a matter of nano-seconds, the same STM may take many seconds to perform the same operation using eight thousand bit inputs.